A, B:Type, g:(A(B + Top)), X:MaInterface(A), es:ES, e:E.
ma-in-interface(es;ma-interface-compose(g;X);e) ~ ma-in-interface(es;X;e) 

latex

Definitions	fpf dom compose compseq tag def, x:A  B(x), {x:A| B(x)} , Knd, b, t  T, Top, left + right, x:AB(x), x:A. B(x), State(ds), Type, hasloc(k;i), x. t(x), a:A fp B(a), Id, P  Q, f(x), s = t, <a, b>, , {T}, SQType(T), s ~ t, A, P & Q, P  Q, Unit, fpf ap compose compseq tag def, ma-in-interface(es;X;e), ma-interface-compose(g;X), MaInterface(T), E, ES, loc(e), IdDeq, x  dom(f)
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool sq, fpf-ap wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf